The sections that follow list all the theorems built into the \HOL\ system.
These include theorems proved and bound to \ML\ identifiers when the system is
built, and theorems proved when the system is built and then stored in a
built-in theory file.  The latter are usually (but not always) set up to
autoload when their names are mentioned in \ML.

Theorems are listed in alphabetical order, by the name of the \ML\ identifier
to which they are bound or the name under which they are stored in a built-in
theory file.  Theory names are given after the names of theorems, in
parentheses. The theory name `{\it none}' indicates that the theorem in
question is not stored in any built-in theory.
